minus(minus(x)) → x
minus(h(x)) → h(minus(x))
minus(f(x, y)) → f(minus(y), minus(x))
↳ QTRS
↳ DependencyPairsProof
minus(minus(x)) → x
minus(h(x)) → h(minus(x))
minus(f(x, y)) → f(minus(y), minus(x))
MINUS(h(x)) → MINUS(x)
MINUS(f(x, y)) → MINUS(y)
MINUS(f(x, y)) → MINUS(x)
minus(minus(x)) → x
minus(h(x)) → h(minus(x))
minus(f(x, y)) → f(minus(y), minus(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
MINUS(h(x)) → MINUS(x)
MINUS(f(x, y)) → MINUS(y)
MINUS(f(x, y)) → MINUS(x)
minus(minus(x)) → x
minus(h(x)) → h(minus(x))
minus(f(x, y)) → f(minus(y), minus(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(h(x)) → MINUS(x)
MINUS(f(x, y)) → MINUS(y)
MINUS(f(x, y)) → MINUS(x)
The value of delta used in the strict ordering is 1.
POL(f(x1, x2)) = 3/2 + (4)x_1 + (4)x_2
POL(h(x1)) = 1/4 + (11/4)x_1
POL(MINUS(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
minus(minus(x)) → x
minus(h(x)) → h(minus(x))
minus(f(x, y)) → f(minus(y), minus(x))